#formal execution models
Research
Shixin Song*,
Davide Davoli,
Elias Storme,
Marton Bognar,
Dominique Devriese,
Frank Piessens,
Tamara Rezk
Jan 1st 2026
The ACM Conference on Computer and Communications Security (CCS) 2026
Developed a formal framework for reasoning jointly about capability safety, speculative execution, and information-flow security; presented SCHERI, a new processor design within this framework; and formally proved that SCHERI provides end-to-end secure speculation guarantees under the constant-time policy.